|
In proof theory, a branch of mathematical logic, elementary function arithmetic, also called EFA, elementary arithmetic and exponential function arithmetic, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, ''x''''y'', together with induction for formulas with bounded quantifiers. EFA is a very weak logical system, whose proof theoretic ordinal is ω3, but still seems able to prove much of ordinary mathematics that can be stated in the language of first-order arithmetic. ==Definition== EFA is a system in first order logic (with equality). Its language contains: *two constants 0, 1, *three binary operations +, ×, exp, with exp(''x'',''y'') usually written as ''x''''y'', *a binary relation symbol < (This is not really necessary as it can be written in terms of the other operations and is sometimes omitted, but is convenient for defining bounded quantifiers). Bounded quantifiers are those of the form ∀(x *The axioms of Robinson arithmetic for 0, 1, +, ×, < *The axioms for exponentiation: ''x''0 = 1, ''x''''y''+1 = ''x''''y''×''x''. *Induction for formulas all of whose quantifiers are bounded (but which may contain free variables). 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Elementary function arithmetic」の詳細全文を読む スポンサード リンク
|